package ch.epfl.lara.matcheck.verify.spec;

import ch.epfl.lara.matcheck.ast.{Imply,And,Formula}
import ch.epfl.lara.matcheck.verify.provers.ProverResults
import ch.epfl.lara.matcheck.util.printer.PrettyStringerFormula

abstract class SpecVerifier {

  private var last_proved: Formula = _
  
  protected def prove(f: Option[Formula]): ProverResults.ProverResult = f match {
    case None => ProverResults.Valid
    case Some(f) => prove(f)
  }
  
  protected def prove(f: Formula): ProverResults.ProverResult = {
    startTimer()
    val res = Config.PROVER(f)
    stopTimer()
    last_formula_proved = f
    res
  }
  
  protected def debug(f: Formula) {
    Report.debug("\n"+Config.PROVER.asString(f)+"\n")
  }
  
  //def verify(): Unit

  protected def startTimer(): Unit
  protected def stopTimer(): Unit
  
  /** getters & setters*/
  /*def axioms_=(a: Formula) = _axioms = a
  def axioms: Formula = _axioms*/
  
  
  def last_formula_proved = last_proved
  def last_formula_proved_=(f: Formula) = last_proved = f
}
